Nuprl Lemma : l_contains_nil
11,40
postcript
pdf
T
:Type,
L
:(
T
List). []
L
latex
Definitions
t
T
,
Type
,
type
List
,
[]
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
{
x
:
A
|
B
(
x
)}
,
,
a
<
b
,
s
=
t
,
,
||
as
||
,
s
~
t
,
{
T
}
,
P
Q
,
False
,
A
,
A
B
,
,
SQType(
T
)
,
x
:
A
B
(
x
)
,
A
c
B
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
x
L
.
P
(
x
)
,
A
B
Lemmas
l
member
wf
origin
T:Type, L:(T List). [] 
L T:Type, L:(T List). [] L 
Tx:A. B(x) l)
Q
A
B
B(x)
B
x:A. B(x)
B(x)xL. P(x) B